Nuprl Definition : l_exists
11,40
postcript
pdf
l_exists(
L
;
T
;
x
.
P
(
x
)) ==
x
:
T
. ((
x
L
)
P
(
x
))
latex
clarification:
l_exists(
L
;
T
;
x
.
P
(
x
)) ==
x
:
T
. ((
x
L
T
)
P
(
x
))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
(
x
l
)
FDL editor aliases
l_exists
origin
x:T. ((x 
L) 
P(x))
x:T. ((x L T) P(x)) x:T. ((x L) P(x))
x:T. ((x L T) P(x)) x:A. B(x) Q l)